$\forall$$w$:World, $a$, $b$:E. w\_locle($w$;$a$;$b$) $\in$ Prop